<html>
<head><meta charset="utf-8"><title>coinduction bug · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html">coinduction bug</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="165013396"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165013396" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165013396">(May 06 2019 at 19:55)</a>:</h4>
<p>So I think the bug would actually show up in this situation:</p>
<div class="codehilite"><pre><span></span>// Send is coinductive:
Send(X) :- Foo(X), Bar(X).
Foo(X) :- Send(X)
</pre></div>



<a name="165013431"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165013431" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165013431">(May 06 2019 at 19:55)</a>:</h4>
<p>If we were (say) solving <code>Send(u32)</code>, then we would go to solve <code>Foo(u32)</code> and conclude that -- since <code>Send(u32)</code> is on the stack -- <code>Foo(u32)</code> is true.</p>



<a name="165013443"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165013443" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165013443">(May 06 2019 at 19:55)</a>:</h4>
<p>But, in fact, we will later disprove <code>Send(u32)</code></p>



<a name="165013522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165013522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165013522">(May 06 2019 at 19:56)</a>:</h4>
<p>If we used a delayed literal instead, then the result of <code>Foo(u32)</code> would be <code>Send(u32) |</code> (i.e., with a delay), and we would ultimately reject it as false.</p>



<a name="165018116"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165018116" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165018116">(May 06 2019 at 20:55)</a>:</h4>
<p>So one thing i'm wondering here though -- can we solve this by always selecting "inductive" goals first?</p>



<a name="165018133"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165018133" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165018133">(May 06 2019 at 20:55)</a>:</h4>
<p>I think I had convinced myself we cannot but now .. I'm wondering why</p>



<a name="165018248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165018248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165018248">(May 06 2019 at 20:56)</a>:</h4>
<p>ah, well, of course</p>



<a name="165018263"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20bug/near/165018263" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20bug.html#165018263">(May 06 2019 at 20:57)</a>:</h4>
<p>all the predicates could be coinductive</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>